package ca.shojaei.mini_sat;

import java.util.Vector;

public class ExistsUntil extends Clause {
	
	private Clause F;
	private Clause G;
	private String symbol = "eU";
	
	public ExistsUntil() {
		super();
		this.unary = false;
		this.evaluable = true;
	}
	
	public ExistsUntil(Clause f, Clause g, String symbol) {
		super();
		F = f;
		G = g;
		this.symbol = symbol;
		this.unary = false;
	}
	
	public Clause getLeft(){
		return getF();
	}
	public void setLeft(Clause c){
		setF(c);
	}
	
	public Clause getRight(){
		return getG();
	}
	public void setRight( Clause c){
		setG(c);
	}
	
	public Clause getF() {
		return F;
	}
	public void setF(Clause f) {
		F = f;
	}
	public Clause getG() {
		return G;
	}
	public void setG(Clause g) {
		G = g;
	}
	public String getSymbol() {
		if(this.negated){
			String str = "!".concat(this.symbol);
			return str;
		}
		return symbol;
	}
	public void setSymbol(String symbol) {
		this.symbol = symbol;
	}

	@Override
	public Vector<int[]> getDIMACS(Model m) {
		// TODO Auto-generated method stub
		return null;
	}

	@Override
	public boolean evaluate(Model m) {
		
		State cur = m.getCurrentStat();
		
		if(G.evaluate(m))
		{
			if(negated)
				return false;
			
			return true;
		}
		
		if(F.evaluate(m))
		{
			boolean out = false;
			
			Vector<State> nexts = m.getCurrentStat().getNexts();
			
			for(int i = 0 ; i < nexts.size(); i++)
			{
				m.setCurrentStat(nexts.get(i).getStateName());
				
				if(until(m, cur, F, G )){
					
					out = true;
					break;
				}
			}
			
			// Set the current state back to what it was
			m.setCurrentStat(cur.getStateName());
			if(negated)
				out = !out;
			return out;
			
		}else
		{
			if(negated)
				return true;
			
    		return false;
		}
	}
	
	private boolean until(Model m, State start, Clause F, Clause G)
	{
		boolean out = false;
		State cur = m.getCurrentStat();
		if(m.getCurrentStat().getStateName() == start.getStateName())
			return false;
		
		if(G.evaluate(m ))
			return true;
		
		if(F.evaluate(m))
		{
			Vector<State> nexts = m.getCurrentStat().getNexts();
			
			for(int i = 0 ; i < nexts.size(); i++)
			{
				m.setCurrentStat(nexts.get(i).getStateName());
				
				if(until(m, cur, F, G )){
					
					out = true;
					break;
				}
			}
			// Set the current state back to what it was
			m.setCurrentStat(cur.getStateName());
			return out;
			
		}else{
			return false;
		}
	}

}
